es:ES, i, x:Id, T:Type, I:(T).
(@i(x:T) c e@i. (first(e))  I(x when e))
 e@i. I(x when e)  I((x after e))
 @i always.I(x) 

latex

Definitions	True, T, x. t(x), t  T, P & Q, @i always.P(x), x(s), e@i. P(e), @i(x:T), A c B, P  Q, , x:A. B(x), {T}, SQType(T), P  Q, P  Q
Lemmas	event system wf, es-isconst wf, es-after wf, Id wf, alle-at wf, es-loc wf, es-first wf, assert wf, not wf, es-pred wf, true wf, squash wf, subtype rel wf, es-loc-pred, Id sq, es-after-pred, es-vartype wf, es-when wf, alle-at-iff